T:Type, as, bs, cs, ds:T List.
(as @ cs) = (bs @ ds)  T List
 ||as|| = ||bs||    ||cs|| = ||ds||  
 {as = bs & cs = ds} 

latex

Definitions	P  Q, {T}, P & Q, P  Q, ||as||, Prop, as @ bs, x:A. B(x), t  T, False, ij, P  Q, P  Q, tl(l), AB, A, hd(l), True
Lemmas	hd wf, ge wf, tl wf, length append, add functionality wrt eq, non neg length, append wf, length wf1